\begin{tabbing}
state\_after($e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=state\_after($e$;$\lambda$$e$.w{-}info($w$;$e$);$\lambda$$e$.w{-}pred($w$;$e$);$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.\+
\\[0ex]1of(2of(w{-}machine($w$;$i$)));$\lambda$$e$.val($e$))
\-
\end{tabbing}